EN FR
EN FR




Section: Software

CoLoR and Rainbow

Participants : Frédéric Blanqui [correspondant] , Kim-Quyen Ly, Sidi Ould Biha.

CoLoR is a Coq [44] library on rewriting theory and termination of nearly 70,000 lines of code [11] . it provides definitions and theorems for:

  • Mathematical structures: relations, (ordered) semi-rings.

  • Data structures: lists, vectors, polynomials with multiple variables, finite multisets, matrices.

  • Term structures: strings, algebraic terms with symbols of fixed arity, algebraic terms with varyadic symbols, simply typed lambda-terms.

  • Transformation techniques: conversion from strings to algebraic terms, conversion from algebraic to varyadic terms, arguments filtering, rule elimination, dependency pairs, dependency graph decomposition, semantic labelling.

  • Termination criteria: polynomial interpretations, multiset ordering, lexicographic ordering, first and higher order recursive path ordering, matrix interpretations.

Rainbow is a tool for automatically certifying termination certificates expressed in the CPF XML format [29] used in the termination competition on termination [32] . Termination certificates are translated and checked in Coq by using the CoLoR library.

CoLoR and Rainbow are distributed under the CeCILL license on http://color.inria.fr/ . Various people participated to its development (see the website for more information).